Search for: All records

Concurrency and causality can be expressed within a labelled transition system by exploiting reversibility of transitions. It is natural to ask what behavioural equivalences can be captured by bisimulations in the reversible setting. In this paper we work with keyed configuration structures and CCSK, establish an operational correspondence between the two models, and give definitions of hereditary history-preserving bisimulation and history-preserving bisimulation in both models. We then present several characterisation results for the two bisimulations in terms of previously proposed, as well as new, “reverse” bisimulations. 

Among the formalisms that can be used to reason about concurrent systems, process calculi stand out both for their simple syntax and close connection to reversibility. They also offer approaches to study relations such as dependence, concurrency or causality between transitions, useful in exploring e.g., causes of bugs or how to multi-thread executions. This paper offers two main contributions: first, we provide separate definitions of a dependence relation and an independence relation, and prove their complementarity on connected transitions instead of postulating it, as is usually done. We also prove that those relations, as well as the notions of event, concurrency, causality and conflict, are unique for any reversible system respecting basic sanity axioms. Second, we prove that the operational definitions of core independence and causality coincide with their characterisations using a pre-existing syntactic mechanism in reversible process calculi, namely communication keys.